$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it In}$:AbsInterface(${\it Cmd}$), $e$:E. \\[0ex]is{-}query(${\it In}$;${\it isupdate}$;$e$) $\in$ $\mathbb{P}$